(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
g(c, g(c, x)) → g(e, g(d, x))
g(d, g(d, x)) → g(c, g(e, x))
g(e, g(e, x)) → g(d, g(c, x))
f(g(x, y)) → g(y, g(f(f(x)), a))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
g(z0, g(z1, g(z0, z1))) → g(a, g(z0, g(z1, b)))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
G(z0, g(z1, g(z0, z1))) → c4(G(a, g(z0, g(z1, b))), G(z0, g(z1, b)), G(z1, b))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
S tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
G(z0, g(z1, g(z0, z1))) → c4(G(a, g(z0, g(z1, b))), G(z0, g(z1, b)), G(z1, b))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c2, c3, c4, c5
(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
G(
z0,
g(
z1,
g(
z0,
z1))) →
c4(
G(
a,
g(
z0,
g(
z1,
b))),
G(
z0,
g(
z1,
b)),
G(
z1,
b)) by
G(x0, g(x1, g(x0, x1))) → c4(G(a, g(x0, g(x1, b))), G(x0, g(x1, b)))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
g(z0, g(z1, g(z0, z1))) → g(a, g(z0, g(z1, b)))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(x0, g(x1, g(x0, x1))) → c4(G(a, g(x0, g(x1, b))), G(x0, g(x1, b)))
S tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(x0, g(x1, g(x0, x1))) → c4(G(a, g(x0, g(x1, b))), G(x0, g(x1, b)))
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c2, c3, c5, c4
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
g(
z0,
z1)) →
c5(
G(
z1,
g(
f(
f(
z0)),
a)),
G(
f(
f(
z0)),
a),
F(
f(
z0)),
F(
z0)) by
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
F(g(x0, x1)) → c5
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
g(z0, g(z1, g(z0, z1))) → g(a, g(z0, g(z1, b)))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
G(x0, g(x1, g(x0, x1))) → c4(G(a, g(x0, g(x1, b))), G(x0, g(x1, b)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
F(g(x0, x1)) → c5
S tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
G(x0, g(x1, g(x0, x1))) → c4(G(a, g(x0, g(x1, b))), G(x0, g(x1, b)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
F(g(x0, x1)) → c5
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c2, c3, c4, c5, c5
(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(g(x0, x1)) → c5
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
g(z0, g(z1, g(z0, z1))) → g(a, g(z0, g(z1, b)))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
G(x0, g(x1, g(x0, x1))) → c4(G(a, g(x0, g(x1, b))), G(x0, g(x1, b)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
S tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
G(x0, g(x1, g(x0, x1))) → c4(G(a, g(x0, g(x1, b))), G(x0, g(x1, b)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c2, c3, c4, c5
(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
g(
g(
z0,
z1),
x1)) →
c5(
G(
x1,
g(
f(
g(
z1,
g(
f(
f(
z0)),
a))),
a)),
G(
f(
f(
g(
z0,
z1))),
a),
F(
f(
g(
z0,
z1))),
F(
g(
z0,
z1))) by
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
g(z0, g(z1, g(z0, z1))) → g(a, g(z0, g(z1, b)))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
G(x0, g(x1, g(x0, x1))) → c4(G(a, g(x0, g(x1, b))), G(x0, g(x1, b)))
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
S tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
G(x0, g(x1, g(x0, x1))) → c4(G(a, g(x0, g(x1, b))), G(x0, g(x1, b)))
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c2, c3, c4, c5, c5
(11) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
G(
x0,
g(
x1,
g(
x0,
x1))) →
c4(
G(
a,
g(
x0,
g(
x1,
b))),
G(
x0,
g(
x1,
b))) by
G(e, g(z1, g(e, z1))) → c4(G(a, g(e, g(z1, b))), G(e, g(z1, b)))
G(d, g(z1, g(d, z1))) → c4(G(a, g(d, g(z1, b))), G(d, g(z1, b)))
G(c, g(z1, g(c, z1))) → c4(G(a, g(c, g(z1, b))), G(c, g(z1, b)))
G(a, g(b, g(a, b))) → c4(G(a, g(a, g(b, b))), G(a, g(b, b)))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
g(z0, g(z1, g(z0, z1))) → g(a, g(z0, g(z1, b)))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
G(e, g(z1, g(e, z1))) → c4(G(a, g(e, g(z1, b))), G(e, g(z1, b)))
G(d, g(z1, g(d, z1))) → c4(G(a, g(d, g(z1, b))), G(d, g(z1, b)))
G(c, g(z1, g(c, z1))) → c4(G(a, g(c, g(z1, b))), G(c, g(z1, b)))
G(a, g(b, g(a, b))) → c4(G(a, g(a, g(b, b))), G(a, g(b, b)))
S tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
G(e, g(z1, g(e, z1))) → c4(G(a, g(e, g(z1, b))), G(e, g(z1, b)))
G(d, g(z1, g(d, z1))) → c4(G(a, g(d, g(z1, b))), G(d, g(z1, b)))
G(c, g(z1, g(c, z1))) → c4(G(a, g(c, g(z1, b))), G(c, g(z1, b)))
G(a, g(b, g(a, b))) → c4(G(a, g(a, g(b, b))), G(a, g(b, b)))
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c2, c3, c5, c5, c4
(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
G(a, g(b, g(a, b))) → c4(G(a, g(a, g(b, b))), G(a, g(b, b)))
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
g(z0, g(z1, g(z0, z1))) → g(a, g(z0, g(z1, b)))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
G(e, g(z1, g(e, z1))) → c4(G(a, g(e, g(z1, b))), G(e, g(z1, b)))
G(d, g(z1, g(d, z1))) → c4(G(a, g(d, g(z1, b))), G(d, g(z1, b)))
G(c, g(z1, g(c, z1))) → c4(G(a, g(c, g(z1, b))), G(c, g(z1, b)))
S tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
G(e, g(z1, g(e, z1))) → c4(G(a, g(e, g(z1, b))), G(e, g(z1, b)))
G(d, g(z1, g(d, z1))) → c4(G(a, g(d, g(z1, b))), G(d, g(z1, b)))
G(c, g(z1, g(c, z1))) → c4(G(a, g(c, g(z1, b))), G(c, g(z1, b)))
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c2, c3, c5, c5, c4
(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
G(
e,
g(
z1,
g(
e,
z1))) →
c4(
G(
a,
g(
e,
g(
z1,
b))),
G(
e,
g(
z1,
b))) by
G(e, g(x0, g(e, x0))) → c4(G(e, g(x0, b)))
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
g(z0, g(z1, g(z0, z1))) → g(a, g(z0, g(z1, b)))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
G(d, g(z1, g(d, z1))) → c4(G(a, g(d, g(z1, b))), G(d, g(z1, b)))
G(c, g(z1, g(c, z1))) → c4(G(a, g(c, g(z1, b))), G(c, g(z1, b)))
G(e, g(x0, g(e, x0))) → c4(G(e, g(x0, b)))
S tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
G(d, g(z1, g(d, z1))) → c4(G(a, g(d, g(z1, b))), G(d, g(z1, b)))
G(c, g(z1, g(c, z1))) → c4(G(a, g(c, g(z1, b))), G(c, g(z1, b)))
G(e, g(x0, g(e, x0))) → c4(G(e, g(x0, b)))
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c2, c3, c5, c5, c4, c4
(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
G(
d,
g(
z1,
g(
d,
z1))) →
c4(
G(
a,
g(
d,
g(
z1,
b))),
G(
d,
g(
z1,
b))) by
G(d, g(x0, g(d, x0))) → c4(G(d, g(x0, b)))
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
g(z0, g(z1, g(z0, z1))) → g(a, g(z0, g(z1, b)))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
G(c, g(z1, g(c, z1))) → c4(G(a, g(c, g(z1, b))), G(c, g(z1, b)))
G(e, g(x0, g(e, x0))) → c4(G(e, g(x0, b)))
G(d, g(x0, g(d, x0))) → c4(G(d, g(x0, b)))
S tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
G(c, g(z1, g(c, z1))) → c4(G(a, g(c, g(z1, b))), G(c, g(z1, b)))
G(e, g(x0, g(e, x0))) → c4(G(e, g(x0, b)))
G(d, g(x0, g(d, x0))) → c4(G(d, g(x0, b)))
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c2, c3, c5, c5, c4, c4
(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
G(
c,
g(
z1,
g(
c,
z1))) →
c4(
G(
a,
g(
c,
g(
z1,
b))),
G(
c,
g(
z1,
b))) by
G(c, g(x0, g(c, x0))) → c4(G(c, g(x0, b)))
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
g(z0, g(z1, g(z0, z1))) → g(a, g(z0, g(z1, b)))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
G(e, g(x0, g(e, x0))) → c4(G(e, g(x0, b)))
G(d, g(x0, g(d, x0))) → c4(G(d, g(x0, b)))
G(c, g(x0, g(c, x0))) → c4(G(c, g(x0, b)))
S tuples:
G(c, g(c, z0)) → c1(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c2(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c3(G(d, g(c, z0)), G(c, z0))
F(g(g(x0, z0), x2)) → c5(G(x2, g(g(g(f(f(x0)), a), g(f(f(z0)), a)), a)), G(f(f(g(x0, z0))), a), F(f(g(x0, z0))), F(g(x0, z0)))
F(g(g(g(z0, z1), x1), x2)) → c5(G(x2, g(f(g(x1, g(f(g(z1, g(f(f(z0)), a))), a))), a)), G(f(f(g(g(z0, z1), x1))), a), F(f(g(g(z0, z1), x1))), F(g(g(z0, z1), x1)))
F(g(g(x0, x1), x2)) → c5(G(f(f(g(x0, x1))), a), F(f(g(x0, x1))))
G(e, g(x0, g(e, x0))) → c4(G(e, g(x0, b)))
G(d, g(x0, g(d, x0))) → c4(G(d, g(x0, b)))
G(c, g(x0, g(c, x0))) → c4(G(c, g(x0, b)))
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c2, c3, c5, c5, c4
(21) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match(-raise)-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 0.
The compatible tree automaton used to show the Match(-raise)-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2]
transitions:
c0() → 0
e0() → 0
d0() → 0
a0() → 0
b0() → 0
g0(0, 0) → 1
f0(0) → 2
(22) BOUNDS(O(1), O(n^1))